# Remote-Run Tutorial This tutorial aims to provide basic understanding of how to start the fm-weck server and how to remotely run tasks on that server. For a more detailed explanation of fm-weck and its main arguments, please refer to [this tutorial](Tutorial.md). # Table of Contents 1. [Client side](#client-side) 2. [Server side](#server-side) ## Client side To start a run remotely, run `fm-weck remote-run` with the same arguments and options as the `fm-weck run` mode, as follows: ```bash $ fm-weck remote-run --help usage: fm-weck remote-run [-h] -p PROPERTY --host HOST [--timelimit TIMELIMIT] [--output-path OUTPUT_PATH] TOOL FILES [FILES ...] positional arguments: TOOL The tool to obtain the container from. Can be the form :. The TOOL is either the name of a bundled tool (c.f. fm-weck --list) or the path to an fm-tools YAML file. FILES Files to pass to the tool. options: -h, --help show this help message and exit -p PROPERTY, --property PROPERTY, --spec PROPERTY Property that is forwarded to the fm-tool. Either a path to a property file or a property name from SV- COMP or Test-Comp. Use fm-weck serve --list to view all properties that can be called by name. --host HOST Specifies the IP address and the port of the server. --timelimit TIMELIMIT Specifies the maximum amount of time to wait for the server to finish a run, in seconds. --output-path OUTPUT_PATH Specifies the location where the incoming files from the server will be stored, relative to the current working directory. ``` In addition to the usual arguments, the `remote-run` expects the `host` option, which represents the address of the server. We can also get the results of the previously started run with the command `fm-weck get-run`, as follows: ```bash $ fm-weck get-run --help usage: fm-weck get-run [-h] --host HOST [--timelimit TIMELIMIT] [--output-path OUTPUT_PATH] RUN-ID positional arguments: RUN-ID The run ID for which to get the result. options: -h, --help show this help message and exit --host HOST Specifies the IP address and the port of the server. --timelimit TIMELIMIT Specifies the maximum amount of time to wait for the server to finish a run, in seconds. --output-path OUTPUT_PATH Specifies the location where the incoming files from the server will be stored, relative to the current working directory. ``` ### Example client calls A typical client call could look like this: ```bash fm-weck remote-run cpachecker:2.3.1 --host localhost:50051 --property unreach-call ./c_program_example.c ``` This command makes a blocking call to the server and waits for the resulting files to be returned. The property and tool can either be names or paths to user defined files. The command also returns the unique ID of the run to the stdout, which can be used with the `fm-weck get-run` command to get the run results. This can be useful if the blocking call returns an empty value due to a time-out or an internal error. It is also possible to specify how long the call will block until it returns, and the path where the server's output files will be stored. ```bash $ fm-weck remote-run cpachecker:2.3.1 --host localhost:50051 --property unreach-call ./c_program_example.c --timelimit 15 --output-path path/to/output Establishing a connection to the server ... Run ID: 12345 $ ``` This command blocks the client for 15 seconds, then returns, regardless of whether the server finished execution. If the result is received, it stores the resulting files at `path/to/output`, relative to the current working directory. If the 15 second time limit is reached before the server finishes the execution, the call returns without the result. In this case, the client can run the following command to try and retrieve the result of the run: ```bash fm-weck get-run 12345 --host localhost:50051 --timelimit 5 --output-path path/to/output ``` ## Server side Starting the server is straightforward: ```bash $ fm-weck server --help usage: fm-weck server [-h] --port PORT --listen IPADDR options: -h, --help show this help message and exit --port PORT Specifies the port number on which the server will listen. --listen IPADDR Specifies the IP address on which the server will listen. ``` Example of starting the server: ```bash $ fm-weck server --port 50051 --listen localhost INFO:fm_weck.grpc_service.server_utils:Server started, listening on 50051 | ```